R-sub{i:l}
R-sub(A; B)
== if Rnone?(A)
== ifthen True
== if Rplus?(A)
== ifthen R-sub{i:l}(Rplus-left(A); B)  R-sub{i:l}(Rplus-right(A); B)
== if Rplus?(B) then R-sub{i:l}(A; Rplus-left(B))  R-sub{i:l}(A; Rplus-right(B)) else A = B fi 

---

clarification:

R-sub{i:l}
R-sub(A; B)
== if Rnone?(A)
== ifthen True
== if Rplus?(A)
== ifthen R-sub{i:l}(Rplus-left(A); B)  R-sub{i:l}(Rplus-right(A); B)
== if Rplus?(B)
== ifthen R-sub{i:l}(A; Rplus-left(B))  R-sub{i:l}(A; Rplus-right(B))
== else A = B  es_realizer{i:l}
== fi 
(recursive) 

latex

Definitions	es_realizer{i:l}, s = t, Rplus-right(x1), f(a), Rplus-left(x1), P  Q, Rplus?(x1), if b then t else f fi , P  Q, True, Rnone?(x1), x.A(x), Y
FDL editor aliases	R-sub